import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertSame;
import static org.junit.Assert.assertTrue;

import java.io.File;
import java.io.IOException;

import model.BasicParameter;
import model.cnf.CNF;
import model.cnf.FileCNF;
import model.solver.IllegalSolverArgumentException;
import model.solver.RSatParameter;
import model.solver.SolverParameter;
import model.solver.SolverResult;
import model.solver.SolverResultStatus;

import org.junit.Before;
import org.junit.Test;

import controller.solver.RSat;

public class TestRSat {

	
	private File solverDirectory;
	private RSat sat ;
	
	@Before
	public void setUp(){
		try {
			solverDirectory = new File("solveur");
			
			sat = new RSat(solverDirectory);
		} catch (IOException e) {
			e.printStackTrace();
			return;
		}
	}
	
	@Test
	public void testRSat(){
		assertTrue("rsat use timeout", sat.hasTimeout());
	}
		
	@Test
	public void testGetCommandLine(){
		String cnfFile = "./tstcnf/unsat.cnf";
		RSatParameter param = sat.getRSatParameter();
		
		
		String[] tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong source", tab[1], cnfFile);
		
		//change timout
		param.setTimeOut(4000);
		
		tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong source", tab[1], cnfFile);
		assertEquals("wrong parameter : wrong arg for timeout", tab[2], "-t");
		assertEquals("wrong parameter : wrong timeout", tab[3], String.valueOf(param.getTimeOut() / 1000));
	
		//change print solution
		param.setPrintSolution(true);
		tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong source", tab[1], cnfFile);
		assertEquals("wrong parameter : wrong arg for timeout", tab[2], "-t");
		assertEquals("wrong parameter : wrong timeout", tab[3], String.valueOf(param.getTimeOut() / 1000));
		assertEquals("wrong parameter : wrong arg for print option", tab[4], "-s");
		
		//verifie applique pas de delay
		param.setTimeOut(BasicParameter.NO_DELAY);
		tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong source", tab[1], cnfFile);
		assertEquals("wrong parameter : wrong arg for print option", tab[2], "-s");
	}
	
	@Test
	public void testDetectUnsat(){
		String cnfFile = "./tstcnf/unsat.cnf";
		CNF cnf;
		try {
			cnf = new FileCNF(cnfFile);
		} catch (Exception e) {
			e.printStackTrace();
			return;
		}
	

		SolverResult res;
		try {
			res = sat.evaluate(cnf);
		} catch (IllegalSolverArgumentException e) {
			e.printStackTrace();
			return;
		}
		assertSame("doesn't detect cnf is unsat", SolverResultStatus.UNSATISFIABLE, res.getStatus());
	}
	
	@Test
	public void testSatInstance(){
		String cnfFile = "./tstcnf/sat.cnf";
		CNF cnf;
		try {
			cnf = new FileCNF(cnfFile);
		} catch (Exception e) {
			e.printStackTrace();
			return;
		}
	

		SolverResult res;
		try {
			res = sat.evaluate(cnf);
		} catch (IllegalSolverArgumentException e) {
			e.printStackTrace();
			return;
		}
	
		assertSame("doesn't detect cnf is sat", SolverResultStatus.SATISFIABLE, res.getStatus());
	}
	

	@Test
	public void testTimeOut(){
		String cnfFile = "./tstcnf/longue.cnf";
		SolverParameter param = sat.getRSatParameter();
		param.setTimeOut(BasicParameter.MIN_DELAY);
		CNF cnf;
		try {
			cnf = new FileCNF(cnfFile);
		} catch (Exception e) {
			e.printStackTrace();
			return;
		}
	

		SolverResult res;
		try {
			res = sat.evaluate(cnf);
		} catch (IllegalSolverArgumentException e) {
			//e.printStackTrace();
			return;
		}
		assertSame("doesn't detect timeout", SolverResultStatus.TIMEOUT_REACHED, res.getStatus());
	}
	
	@Test
	public void testCNFDoesntExist(){
		String cnfFile = "./tstcnf/.cnf";
		CNF cnf;
		try {
			cnf = new FileCNF(cnfFile);
		} catch (Exception e) {
		//	e.printStackTrace();
			return;
		}
	

		SolverResult res;
		try {
			res = sat.evaluate(cnf);
		} catch (IllegalSolverArgumentException e) {
			//e.printStackTrace();
			return;
		}
		assertSame("doesn't detect cnf doesn't exist", SolverResultStatus.PROBLEM, res.getStatus());
	}
}
